(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
q(0(x1)) → p(p(s(s(0(s(s(s(s(x1)))))))))
q(s(x1)) → p(p(s(s(s(s(s(s(r(p(p(s(s(x1)))))))))))))
r(0(x1)) → p(s(p(s(0(p(p(p(s(s(s(x1)))))))))))
r(s(x1)) → p(s(p(s(s(q(p(s(p(s(x1))))))))))
p(p(s(x1))) → p(x1)
p(s(x1)) → x1
p(0(x1)) → 0(s(s(s(x1))))
Rewrite Strategy: INNERMOST
(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)
Converted CpxTRS to CDT
(2) Obligation:
Complexity Dependency Tuples Problem
Rules:
q(0(z0)) → p(p(s(s(0(s(s(s(s(z0)))))))))
q(s(z0)) → p(p(s(s(s(s(s(s(r(p(p(s(s(z0)))))))))))))
r(0(z0)) → p(s(p(s(0(p(p(p(s(s(s(z0)))))))))))
r(s(z0)) → p(s(p(s(s(q(p(s(p(s(z0))))))))))
p(p(s(z0))) → p(z0)
p(s(z0)) → z0
p(0(z0)) → 0(s(s(s(z0))))
Tuples:
Q(0(z0)) → c(P(p(s(s(0(s(s(s(s(z0))))))))), P(s(s(0(s(s(s(s(z0)))))))))
Q(s(z0)) → c1(P(p(s(s(s(s(s(s(r(p(p(s(s(z0))))))))))))), P(s(s(s(s(s(s(r(p(p(s(s(z0)))))))))))), R(p(p(s(s(z0))))), P(p(s(s(z0)))), P(s(s(z0))))
R(0(z0)) → c2(P(s(p(s(0(p(p(p(s(s(s(z0))))))))))), P(s(0(p(p(p(s(s(s(z0))))))))), P(p(p(s(s(s(z0)))))), P(p(s(s(s(z0))))), P(s(s(s(z0)))))
R(s(z0)) → c3(P(s(p(s(s(q(p(s(p(s(z0)))))))))), P(s(s(q(p(s(p(s(z0)))))))), Q(p(s(p(s(z0))))), P(s(p(s(z0)))), P(s(z0)))
P(p(s(z0))) → c4(P(z0))
S tuples:
Q(0(z0)) → c(P(p(s(s(0(s(s(s(s(z0))))))))), P(s(s(0(s(s(s(s(z0)))))))))
Q(s(z0)) → c1(P(p(s(s(s(s(s(s(r(p(p(s(s(z0))))))))))))), P(s(s(s(s(s(s(r(p(p(s(s(z0)))))))))))), R(p(p(s(s(z0))))), P(p(s(s(z0)))), P(s(s(z0))))
R(0(z0)) → c2(P(s(p(s(0(p(p(p(s(s(s(z0))))))))))), P(s(0(p(p(p(s(s(s(z0))))))))), P(p(p(s(s(s(z0)))))), P(p(s(s(s(z0))))), P(s(s(s(z0)))))
R(s(z0)) → c3(P(s(p(s(s(q(p(s(p(s(z0)))))))))), P(s(s(q(p(s(p(s(z0)))))))), Q(p(s(p(s(z0))))), P(s(p(s(z0)))), P(s(z0)))
P(p(s(z0))) → c4(P(z0))
K tuples:none
Defined Rule Symbols:
q, r, p
Defined Pair Symbols:
Q, R, P
Compound Symbols:
c, c1, c2, c3, c4
(3) CdtUnreachableProof (EQUIVALENT transformation)
The following tuples could be removed as they are not reachable from basic start terms:
P(p(s(z0))) → c4(P(z0))
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
q(0(z0)) → p(p(s(s(0(s(s(s(s(z0)))))))))
q(s(z0)) → p(p(s(s(s(s(s(s(r(p(p(s(s(z0)))))))))))))
r(0(z0)) → p(s(p(s(0(p(p(p(s(s(s(z0)))))))))))
r(s(z0)) → p(s(p(s(s(q(p(s(p(s(z0))))))))))
p(p(s(z0))) → p(z0)
p(s(z0)) → z0
p(0(z0)) → 0(s(s(s(z0))))
Tuples:
Q(0(z0)) → c(P(p(s(s(0(s(s(s(s(z0))))))))), P(s(s(0(s(s(s(s(z0)))))))))
Q(s(z0)) → c1(P(p(s(s(s(s(s(s(r(p(p(s(s(z0))))))))))))), P(s(s(s(s(s(s(r(p(p(s(s(z0)))))))))))), R(p(p(s(s(z0))))), P(p(s(s(z0)))), P(s(s(z0))))
R(0(z0)) → c2(P(s(p(s(0(p(p(p(s(s(s(z0))))))))))), P(s(0(p(p(p(s(s(s(z0))))))))), P(p(p(s(s(s(z0)))))), P(p(s(s(s(z0))))), P(s(s(s(z0)))))
R(s(z0)) → c3(P(s(p(s(s(q(p(s(p(s(z0)))))))))), P(s(s(q(p(s(p(s(z0)))))))), Q(p(s(p(s(z0))))), P(s(p(s(z0)))), P(s(z0)))
S tuples:
Q(0(z0)) → c(P(p(s(s(0(s(s(s(s(z0))))))))), P(s(s(0(s(s(s(s(z0)))))))))
Q(s(z0)) → c1(P(p(s(s(s(s(s(s(r(p(p(s(s(z0))))))))))))), P(s(s(s(s(s(s(r(p(p(s(s(z0)))))))))))), R(p(p(s(s(z0))))), P(p(s(s(z0)))), P(s(s(z0))))
R(0(z0)) → c2(P(s(p(s(0(p(p(p(s(s(s(z0))))))))))), P(s(0(p(p(p(s(s(s(z0))))))))), P(p(p(s(s(s(z0)))))), P(p(s(s(s(z0))))), P(s(s(s(z0)))))
R(s(z0)) → c3(P(s(p(s(s(q(p(s(p(s(z0)))))))))), P(s(s(q(p(s(p(s(z0)))))))), Q(p(s(p(s(z0))))), P(s(p(s(z0)))), P(s(z0)))
K tuples:none
Defined Rule Symbols:
q, r, p
Defined Pair Symbols:
Q, R
Compound Symbols:
c, c1, c2, c3
(5) CdtGraphRemoveDanglingProof (ComplexityIfPolyImplication transformation)
Removed 2 of 4 dangling nodes:
Q(0(z0)) → c(P(p(s(s(0(s(s(s(s(z0))))))))), P(s(s(0(s(s(s(s(z0)))))))))
R(0(z0)) → c2(P(s(p(s(0(p(p(p(s(s(s(z0))))))))))), P(s(0(p(p(p(s(s(s(z0))))))))), P(p(p(s(s(s(z0)))))), P(p(s(s(s(z0))))), P(s(s(s(z0)))))
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
q(0(z0)) → p(p(s(s(0(s(s(s(s(z0)))))))))
q(s(z0)) → p(p(s(s(s(s(s(s(r(p(p(s(s(z0)))))))))))))
r(0(z0)) → p(s(p(s(0(p(p(p(s(s(s(z0)))))))))))
r(s(z0)) → p(s(p(s(s(q(p(s(p(s(z0))))))))))
p(p(s(z0))) → p(z0)
p(s(z0)) → z0
p(0(z0)) → 0(s(s(s(z0))))
Tuples:
Q(s(z0)) → c1(P(p(s(s(s(s(s(s(r(p(p(s(s(z0))))))))))))), P(s(s(s(s(s(s(r(p(p(s(s(z0)))))))))))), R(p(p(s(s(z0))))), P(p(s(s(z0)))), P(s(s(z0))))
R(s(z0)) → c3(P(s(p(s(s(q(p(s(p(s(z0)))))))))), P(s(s(q(p(s(p(s(z0)))))))), Q(p(s(p(s(z0))))), P(s(p(s(z0)))), P(s(z0)))
S tuples:
Q(s(z0)) → c1(P(p(s(s(s(s(s(s(r(p(p(s(s(z0))))))))))))), P(s(s(s(s(s(s(r(p(p(s(s(z0)))))))))))), R(p(p(s(s(z0))))), P(p(s(s(z0)))), P(s(s(z0))))
R(s(z0)) → c3(P(s(p(s(s(q(p(s(p(s(z0)))))))))), P(s(s(q(p(s(p(s(z0)))))))), Q(p(s(p(s(z0))))), P(s(p(s(z0)))), P(s(z0)))
K tuples:none
Defined Rule Symbols:
q, r, p
Defined Pair Symbols:
Q, R
Compound Symbols:
c1, c3
(7) CdtGraphRemoveTrailingProof (BOTH BOUNDS(ID, ID) transformation)
Removed 8 trailing tuple parts
(8) Obligation:
Complexity Dependency Tuples Problem
Rules:
q(0(z0)) → p(p(s(s(0(s(s(s(s(z0)))))))))
q(s(z0)) → p(p(s(s(s(s(s(s(r(p(p(s(s(z0)))))))))))))
r(0(z0)) → p(s(p(s(0(p(p(p(s(s(s(z0)))))))))))
r(s(z0)) → p(s(p(s(s(q(p(s(p(s(z0))))))))))
p(p(s(z0))) → p(z0)
p(s(z0)) → z0
p(0(z0)) → 0(s(s(s(z0))))
Tuples:
Q(s(z0)) → c1(R(p(p(s(s(z0))))))
R(s(z0)) → c3(Q(p(s(p(s(z0))))))
S tuples:
Q(s(z0)) → c1(R(p(p(s(s(z0))))))
R(s(z0)) → c3(Q(p(s(p(s(z0))))))
K tuples:none
Defined Rule Symbols:
q, r, p
Defined Pair Symbols:
Q, R
Compound Symbols:
c1, c3
(9) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
Q(
s(
z0)) →
c1(
R(
p(
p(
s(
s(
z0)))))) by
Q(s(x0)) → c1(R(p(s(x0))))
(10) Obligation:
Complexity Dependency Tuples Problem
Rules:
q(0(z0)) → p(p(s(s(0(s(s(s(s(z0)))))))))
q(s(z0)) → p(p(s(s(s(s(s(s(r(p(p(s(s(z0)))))))))))))
r(0(z0)) → p(s(p(s(0(p(p(p(s(s(s(z0)))))))))))
r(s(z0)) → p(s(p(s(s(q(p(s(p(s(z0))))))))))
p(p(s(z0))) → p(z0)
p(s(z0)) → z0
p(0(z0)) → 0(s(s(s(z0))))
Tuples:
R(s(z0)) → c3(Q(p(s(p(s(z0))))))
Q(s(x0)) → c1(R(p(s(x0))))
S tuples:
R(s(z0)) → c3(Q(p(s(p(s(z0))))))
Q(s(x0)) → c1(R(p(s(x0))))
K tuples:none
Defined Rule Symbols:
q, r, p
Defined Pair Symbols:
R, Q
Compound Symbols:
c3, c1
(11) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
R(
s(
z0)) →
c3(
Q(
p(
s(
p(
s(
z0)))))) by
R(s(x0)) → c3(Q(p(s(x0))))
(12) Obligation:
Complexity Dependency Tuples Problem
Rules:
q(0(z0)) → p(p(s(s(0(s(s(s(s(z0)))))))))
q(s(z0)) → p(p(s(s(s(s(s(s(r(p(p(s(s(z0)))))))))))))
r(0(z0)) → p(s(p(s(0(p(p(p(s(s(s(z0)))))))))))
r(s(z0)) → p(s(p(s(s(q(p(s(p(s(z0))))))))))
p(p(s(z0))) → p(z0)
p(s(z0)) → z0
p(0(z0)) → 0(s(s(s(z0))))
Tuples:
Q(s(x0)) → c1(R(p(s(x0))))
R(s(x0)) → c3(Q(p(s(x0))))
S tuples:
Q(s(x0)) → c1(R(p(s(x0))))
R(s(x0)) → c3(Q(p(s(x0))))
K tuples:none
Defined Rule Symbols:
q, r, p
Defined Pair Symbols:
Q, R
Compound Symbols:
c1, c3
(13) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
Q(
s(
x0)) →
c1(
R(
p(
s(
x0)))) by
Q(s(z0)) → c1(R(z0))
(14) Obligation:
Complexity Dependency Tuples Problem
Rules:
q(0(z0)) → p(p(s(s(0(s(s(s(s(z0)))))))))
q(s(z0)) → p(p(s(s(s(s(s(s(r(p(p(s(s(z0)))))))))))))
r(0(z0)) → p(s(p(s(0(p(p(p(s(s(s(z0)))))))))))
r(s(z0)) → p(s(p(s(s(q(p(s(p(s(z0))))))))))
p(p(s(z0))) → p(z0)
p(s(z0)) → z0
p(0(z0)) → 0(s(s(s(z0))))
Tuples:
R(s(x0)) → c3(Q(p(s(x0))))
Q(s(z0)) → c1(R(z0))
S tuples:
R(s(x0)) → c3(Q(p(s(x0))))
Q(s(z0)) → c1(R(z0))
K tuples:none
Defined Rule Symbols:
q, r, p
Defined Pair Symbols:
R, Q
Compound Symbols:
c3, c1
(15) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
R(s(x0)) → c3(Q(p(s(x0))))
We considered the (Usable) Rules:
p(s(z0)) → z0
And the Tuples:
R(s(x0)) → c3(Q(p(s(x0))))
Q(s(z0)) → c1(R(z0))
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(Q(x1)) = [4]x1
POL(R(x1)) = [2] + [4]x1
POL(c1(x1)) = x1
POL(c3(x1)) = x1
POL(p(x1)) = x1
POL(s(x1)) = [4] + x1
(16) Obligation:
Complexity Dependency Tuples Problem
Rules:
q(0(z0)) → p(p(s(s(0(s(s(s(s(z0)))))))))
q(s(z0)) → p(p(s(s(s(s(s(s(r(p(p(s(s(z0)))))))))))))
r(0(z0)) → p(s(p(s(0(p(p(p(s(s(s(z0)))))))))))
r(s(z0)) → p(s(p(s(s(q(p(s(p(s(z0))))))))))
p(p(s(z0))) → p(z0)
p(s(z0)) → z0
p(0(z0)) → 0(s(s(s(z0))))
Tuples:
R(s(x0)) → c3(Q(p(s(x0))))
Q(s(z0)) → c1(R(z0))
S tuples:
Q(s(z0)) → c1(R(z0))
K tuples:
R(s(x0)) → c3(Q(p(s(x0))))
Defined Rule Symbols:
q, r, p
Defined Pair Symbols:
R, Q
Compound Symbols:
c3, c1
(17) CdtKnowledgeProof (EQUIVALENT transformation)
The following tuples could be moved from S to K by knowledge propagation:
Q(s(z0)) → c1(R(z0))
R(s(x0)) → c3(Q(p(s(x0))))
Now S is empty
(18) BOUNDS(O(1), O(1))